
#include "app.h"

LRESULT APIENTRY WndProc(HWND hwnd, UINT iMsg, WPARAM wParam, LPARAM lParam);

solver::problem_solver *current_problem;
char filename[MAX_PATH];
OPENFILENAME openfilename;
threading::job_queue_type job_queue;

#define WM_SOLUTION_STEP (WM_USER+1)
#define WM_SOLUTION_LOADED (WM_USER+2)
#define WM_SOLUTION_NOTE (WM_USER+3)

bool running = false;

int CALLBACK WinMain(
	HINSTANCE hInstance,
	HINSTANCE hPrevInstance,
	LPSTR lpCmdLine,
	int nCmdShow)
{
	MSG msg;
	WNDCLASSEX wc;
	HWND hwnd;

	current_problem = nullptr;
	ZeroMemory(&openfilename, sizeof(OPENFILENAME));
	openfilename.hInstance = hInstance;
	openfilename.lpstrFilter = "DIMACS SAT Problem File\0*.CNF\0\0";
	openfilename.lStructSize = sizeof(OPENFILENAME);
	openfilename.lpstrCustomFilter = nullptr;
	openfilename.lpstrFile = filename;
	openfilename.nMaxFile = sizeof(filename) / sizeof(filename[0]);
	openfilename.Flags = OFN_FILEMUSTEXIST;
	ZeroMemory(filename, sizeof(filename));

	ZeroMemory(&wc, sizeof(wc));
	wc.cbSize = sizeof(wc);
	wc.hInstance = hInstance;
	wc.style = CS_HREDRAW | CS_VREDRAW;
	wc.lpfnWndProc = WndProc;
	wc.lpszClassName = "OverSATDialogClass";
	wc.hbrBackground = (HBRUSH)(COLOR_BTNFACE + 1);
	wc.hIcon = LoadIcon(hInstance, IDI_APPLICATION);
	wc.hIconSm = LoadIcon(hInstance, IDI_APPLICATION);
	wc.hCursor = LoadCursor(NULL, IDC_ARROW);
	wc.lpszMenuName = NULL;
	wc.cbClsExtra = 0;
	wc.cbWndExtra = DLGWINDOWEXTRA;    /* special */

	RegisterClassEx(&wc);

	hwnd = CreateDialog(hInstance, "OverSATDialogBox", 0, NULL);

	ShowWindow(hwnd, nCmdShow);

	job_queue.start(0);

	while (GetMessage(&msg, NULL, 0, 0))
	{
		if (!IsDialogMessage(hwnd, &msg))
		{
			TranslateMessage(&msg);
			DispatchMessage(&msg);
		}
	}

	job_queue.kill();

	return msg.wParam;
}


std::string ProductionToString(solver::problem_solver* cur_problem, solver::production *cur_prod)
{
	std::string implication_text = "";

	if (cur_prod->product.ref == -1)
	{
		implication_text = "Conflict <- ";
	}
	else
	{
		auto& v = cur_problem->variables[cur_prod->product.ref];
		if (cur_prod->product.val == 0)
		{
			implication_text += "!";
		}
		implication_text += std::to_string(v.name);
		implication_text += " <- ";
	}

	implication_text += cur_problem->to_string(cur_prod->match, " ");

	return implication_text;
}

std::string DecisionToString(solver::problem_solver* cur_problem, solver::decision& d, bool connector)
{
	std::string text;

	text = "(";

	for (int i = 0; i < d.literals.size(); i++)
	{
		auto& l = d.literals[i];
		auto& v = cur_problem->variables[l.ref];

		if (d.selected_literal == i) {
			text += "*";
		}

		if (l.val == 0)
		{
			text += "!";
			text += std::to_string(v.name);
		}
		else {
			text += std::to_string(v.name);
		}

		if (i < d.literals.size() - 1) {
			text += " V ";
		}
	}

	if (connector) {
		text += ") ^";
	}
	else 
	{
		text += ")";
	}

	return text;
}


void RenderCurrentProblem(HWND hwnd, solver::problem_solver *current_problem)
{
	if (!current_problem)
		return;
	::SetDlgItemText(hwnd, IDC_EDIT_CNF, "");
	std::string cnf = "";
	for (int i = 0; i < current_problem->decisions.size(); i++)
	{
		if (i) cnf += " ";
		cnf += DecisionToString(current_problem, *(current_problem->decisions[i]), false);
		cnf += "\r\n";
	}
	::SetDlgItemText(hwnd, IDC_EDIT_CNF, cnf.c_str());

	::SendDlgItemMessage(hwnd, IDC_EDIT_GRAMMAR, WM_CLEAR, 0, 0);
	std::string grammar = "";
	for (int i = 0; i < current_problem->productions.size(); i++)
	{
		if (current_problem->productions[i]) {
			grammar += ProductionToString(current_problem, current_problem->productions[i]);
			grammar += "\r\n";
		}
	}
	::SetDlgItemText(hwnd, IDC_EDIT_GRAMMAR, grammar.c_str());
	::SetDlgItemText(hwnd, IDC_EDIT_SOLUTION, "");
}

void RenderStep(HWND hwnd, solver::problem_solver *current_problem)
{
	if (!current_problem)
		return;

	::EnableWindow(GetDlgItem(hwnd, IDC_LOAD_FILE), true);
	::EnableWindow(GetDlgItem(hwnd, IDC_BROWSE_FILE), true);

	::SendDlgItemMessage(hwnd, IDC_EDIT_CNF, WM_CLEAR, 0, 0);
	std::string cnf = "";
	for (int i = 0; i < current_problem->decisions.size(); i++)
	{
		if (i) cnf += " ";
		cnf += DecisionToString(current_problem, *(current_problem->decisions[i]), false);
		cnf += "\r\n";
	}
	::SetDlgItemText(hwnd, IDC_EDIT_CNF, cnf.c_str());

	std::string current_decision = current_problem->to_string(current_problem->solution,"\r\n");
	::SendDlgItemMessage(hwnd, IDC_EDIT_SOLUTION, WM_CLEAR, 0, 0);
	::SetDlgItemText(hwnd, IDC_EDIT_SOLUTION, current_decision.c_str());
	if (current_problem->last_step_result.solved)
	{
		::SetDlgItemText(hwnd, IDC_STATIC_STATUS, "Solved");
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RESET), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_STEP), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RUN), false);

	}
	else if (current_problem->last_step_result.unsolveable)
	{
		::SetDlgItemText(hwnd, IDC_STATIC_STATUS, current_problem->last_step_result.reason.c_str());
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RESET), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_STEP), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RUN), false);
	}
	else 
	{
		char buff[256];
		sprintf(buff, "Stepping: %d decisions", current_problem->solution.size());
		::SetDlgItemText(hwnd, IDC_STATIC_STATUS, buff);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RESET), true);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_STEP), true);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RUN), true);
	}
}


class initializationWorker : public threading::job_type
{
	HWND hwnd;
	solver::file_data fd;

public:

	initializationWorker(HWND hwnd, solver::file_data file_data) :hwnd(hwnd), fd(file_data)
	{
		::EnableWindow(GetDlgItem(hwnd, IDC_LOAD_FILE), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_BROWSE_FILE), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RESET), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_STEP), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RUN), false);
	}

	virtual threading::job_notify_type execute(threading::job_queue_type *_callingQueue, DWORD _bytesTransferred, BOOL _success)
	{
		threading::job_notify_type jnt;
		jnt.setPostMsg(hwnd, WM_SOLUTION_LOADED, 0, 0);
		jnt.shouldDelete = true;
		sat::cnf_sat_solver factory;
		if (current_problem) {
			delete current_problem;
			current_problem = nullptr;
		}
		current_problem = factory.create_problem(fd, [this](const char *str) {
			::SetDlgItemText( hwnd, IDC_STATIC_STATUS, str);
		});
		HWND hCapture = hwnd;
		current_problem->progress_func = [this,hCapture](const char *str) {
			char *cpy = ::strdup(str);
			::PostMessage(hCapture, WM_SOLUTION_NOTE, 0, (LPARAM)cpy);
		};
		return jnt;
	}
};

class calculationWorker : public threading::job_type
{
	HWND hwnd;
	solver::problem_solver *current_problem;

public:

	calculationWorker(HWND hwnd, solver::problem_solver *current_problem) :hwnd(hwnd), current_problem(current_problem)
	{
		::EnableWindow(GetDlgItem(hwnd, IDC_LOAD_FILE), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_BROWSE_FILE), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RESET), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_STEP), false);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RUN), false);
	}

	virtual threading::job_notify_type execute(threading::job_queue_type *_callingQueue, DWORD _bytesTransferred, BOOL _success)
	{
		threading::job_notify_type jnt;
		jnt.setPostMsg(hwnd, WM_SOLUTION_STEP, 0, 0);
		jnt.shouldDelete = true;
		sat::sat_solver_strategy strategy;
		current_problem->step(strategy);
		return jnt;
	}
};

void BrowseAndLoadFile(HWND hwnd)
{
	openfilename.hwndOwner = hwnd;
	if (::GetOpenFileName(&openfilename)) {
		::SetDlgItemText(hwnd, IDC_EDIT_FILENAME, filename);
		::SetDlgItemText(hwnd, IDC_STATIC_STATUS, "Loading");
		solver::file_data fd(filename);
		if (fd.get_error())
		{
			::MessageBox(hwnd, "Could not open file.", "Error", MB_ICONERROR | MB_OK);
		}
		else {
			initializationWorker *worker = new initializationWorker(hwnd, fd);
			job_queue.postJobMessage(worker);
		}
	}
	else {
		auto err = ::CommDlgExtendedError();
		if (err) {
			char buff[512];
			::FormatMessage(FORMAT_MESSAGE_FROM_SYSTEM, NULL, err, 0, buff, sizeof(buff) / sizeof(buff[0]), NULL);
			::MessageBox(hwnd, buff, "Could not open file", MB_ICONEXCLAMATION | MB_OK);
		}
	}
}

void LoadFile(HWND hwnd)
{
	sat::cnf_sat_solver factory;
	::GetDlgItemText(hwnd, IDC_EDIT_FILENAME, filename, sizeof(filename) / sizeof(filename[0]));
	solver::file_data fd(filename);
	if (fd.get_error())
	{
		::MessageBox(hwnd, "Could not open file.", "Error", MB_ICONERROR | MB_OK);
	}
	else {
		initializationWorker *worker = new initializationWorker(hwnd, fd);
		job_queue.postJobMessage(worker);
	}
}

LRESULT APIENTRY WndProc(HWND hwnd, UINT iMsg, WPARAM wParam, LPARAM lParam)
{
	switch (iMsg)
	{
	case WM_SOLUTION_NOTE:
		{
			char *c = (char *)lParam;
			if (c != nullptr) 
			{
				::SetDlgItemText(hwnd, IDC_STATIC_STATUS2, c);
			}
		}
		break;
	case WM_DESTROY:
		PostQuitMessage(0);
		break;
	case WM_SOLUTION_STEP:
		if (current_problem != nullptr)
		{
			::RenderStep(hwnd, current_problem);
			if (running && current_problem != nullptr && current_problem->last_step_result.unsolveable == false && current_problem->last_step_result.solved == false)
			{
				calculationWorker *worker = new calculationWorker(hwnd, current_problem);
				job_queue.postJobMessage(worker);
			}
		}
		break;
	case WM_SOLUTION_LOADED:
		::EnableWindow(GetDlgItem(hwnd, IDC_LOAD_FILE), true);
		::EnableWindow(GetDlgItem(hwnd, IDC_BROWSE_FILE), true);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RESET), true);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_STEP), true);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RESET), true);
		::EnableWindow(GetDlgItem(hwnd, IDC_RUN_RUN), true);
		::SetDlgItemText(hwnd, IDC_STATIC_STATUS, "Loaded");
		if (current_problem != nullptr)
		{
			::RenderCurrentProblem(hwnd, current_problem);
		}
		break;
	case WM_COMMAND:
	{
		int controlid = LOWORD(wParam);
		int notificationid = HIWORD(wParam);

		switch (notificationid)
		{
		case BN_CLICKED:
			switch (controlid)
			{
			case IDC_BROWSE_FILE:
				filename[0] = 0;
				::BrowseAndLoadFile(hwnd);
				break;
			case IDC_LOAD_FILE:
				::LoadFile(hwnd);
				::RenderStep(hwnd, current_problem);
				break;
			case IDC_RUN_RESET:
				running = false;
				if (current_problem != nullptr)
				{
					current_problem->clear();
					::RenderStep(hwnd, current_problem);
				}
				break;
			case IDC_RUN_STEP:
				running = false;
				if (current_problem != nullptr)
				{
					calculationWorker *worker = new calculationWorker(hwnd, current_problem);
					job_queue.postJobMessage(worker);
				}
				break;
			case IDC_RUN_RUN:
				running = !running;
				if (running)
				{
					if (current_problem != nullptr)
					{
						calculationWorker *worker = new calculationWorker(hwnd, current_problem);
						job_queue.postJobMessage(worker);
					}
				}

				break;
			}
			break;
		}
	}
	break;
	default:
		return DefWindowProc(hwnd, iMsg, wParam, lParam);
	}

	return 0;
}
